


@article{DBLP:journals/ijfcs/AbdullaDR11,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Automatic Verification of Directory-Based Consistency Protocols
               with Graph Constraints},
  journal   = {International Journal of Foundations of Computer Science},
  volume    = {22},
  number    = {4},
  year      = {2011},
  pages     = {761-782},
  ee        = {http://dx.doi.org/10.1142/S0129054111008416},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/BouajjaniDERS10,
  author    = {Ahmed Bouajjani and
               Cezara Dragoi and
               Constantin Enea and
               Ahmed Rezine and
               Mihaela Sighireanu},
  title     = {Invariant Synthesis for Programs Manipulating Lists with
               Unbounded Data},
  booktitle = {Computer Aided Verification, 22nd International Conference,
               CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
  year      = {2010},
  pages     = {72-88},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14295-6_8},
  crossref  = {DBLP:conf/cav/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2010,
  editor    = {Tayssir Touili and
               Byron Cook and
               Paul Jackson},
  title     = {Computer Aided Verification, 22nd International Conference,
               CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6174},
  year      = {2010},
  isbn      = {978-3-642-14294-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14295-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{monotonic:cegar,
  author    = {Parosh Aziz Abdulla and
               Yu-Fang Chen and
               Giorgio Delzanno and
               Fr{\'e}d{\'e}ric Haziza and
               Chih-Duo Hong and
               Ahmed Rezine},
  title     = {Constrained Monotonic Abstraction: A CEGAR for Parameterized
               Verification},
  booktitle = {CONCUR 2010 - Concurrency Theory, 21th International Conference},
  year      = {2010},
  pages     = {86-101}
}

@Comment  crossref  = {DBLP:conf/concur/2010},
@Comment CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings},
@Comment  ee        = {http://dx.doi.org/10.1007/978-3-642-15375-4_7},
@Comment  bibsource = {DBLP, http://dblp.uni-trier.de}

@proceedings{DBLP:conf/concur/2010,
  editor    = {Paul Gastin and
               Fran\c{c}ois Laroussinie},
  title     = {CONCUR 2010 - Concurrency Theory, 21th International Conference,
               CONCUR 2010, Paris, France, August 31-September 3, 2010.
               Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6269},
  year      = {2010},
  isbn      = {978-3-642-15374-7},
  ee        = {http://dx.doi.org/10.1007/978-3-642-15375-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/forte/AbdullaDR09,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Approximated Context-Sensitive Analysis for Parameterized
               Verification},
  booktitle = {Formal Techniques for Distributed Systems, Joint 11th IFIP
               WG 6.1 International Conference FMOODS 2009 and 29th IFIP
               WG 6.1 International Conference FORTE 2009, Lisboa, Portugal,
               June 9-12, 2009. Proceedings},
  year      = {2009},
  pages     = {41-56},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02138-1_3},
  crossref  = {DBLP:conf/forte/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/forte/2009,
  editor    = {David Lee and
               Ant{\'o}nia Lopes and
               Arnd Poetzsch-Heffter},
  title     = {Formal Techniques for Distributed Systems, Joint 11th IFIP
               WG 6.1 International Conference FMOODS 2009 and 29th IFIP
               WG 6.1 International Conference FORTE 2009, Lisboa, Portugal,
               June 9-12, 2009. Proceedings},
  booktitle = {FMOODS/FORTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5522},
  year      = {2009},
  isbn      = {978-3-642-02137-4},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02138-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/rp/AbdullaDR09,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Automatic Verification of Directory-Based Consistency Protocols},
  booktitle = {Reachability Problems, 3rd International Workshop, RP 2009,
               Palaiseau, France, September 23-25, 2009. Proceedings},
  year      = {2009},
  pages     = {36-50},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04420-5_6},
  crossref  = {DBLP:conf/rp/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rp/2009,
  editor    = {Olivier Bournez and
               Igor Potapov},
  title     = {Reachability Problems, 3rd International Workshop, RP 2009,
               Palaiseau, France, September 23-25, 2009. Proceedings},
  booktitle = {RP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5797},
  year      = {2009},
  isbn      = {978-3-642-04419-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04420-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/fmsd/AbdullaDR09,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Approximated parameterized verification of infinite-state
               processes with global conditions},
  journal   = {Formal Methods in System Design},
  volume    = {34},
  number    = {2},
  year      = {2009},
  pages     = {126-156},
  ee        = {http://dx.doi.org/10.1007/s10703-008-0062-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/ijfcs/AbdullaDHR09,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Noomene Ben Henda and
               Ahmed Rezine},
  title     = {Monotonic Abstraction: on Efficient Verification of Parameterized
               Systems},
  journal   = {International Journal of Foundations of Computer Science},
  volume    = {20},
  number    = {5},
  year      = {2009},
  pages     = {779-801},
  ee        = {http://dx.doi.org/10.1142/S0129054109006887},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/AbdullaBCHR08,
  author    = {Parosh Aziz Abdulla and
               Ahmed Bouajjani and
               Jonathan Cederberg and
               Fr{\'e}d{\'e}ric Haziza and
               Ahmed Rezine},
  title     = {Monotonic Abstraction for Programs with Dynamic Memory Heaps},
  booktitle = {Computer Aided Verification, 20th International Conference,
               CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
  year      = {2008},
  pages     = {341-354},
  ee        = {http://dx.doi.org/10.1007/978-3-540-70545-1_33},
  crossref  = {DBLP:conf/cav/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2008,
  editor    = {Aarti Gupta and
               Sharad Malik},
  title     = {Computer Aided Verification, 20th International Conference,
               CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5123},
  year      = {2008},
  isbn      = {978-3-540-70543-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/forte/AbdullaHDHR08,
  author    = {Parosh Aziz Abdulla and
               Noomene Ben Henda and
               Giorgio Delzanno and
               Fr{\'e}d{\'e}ric Haziza and
               Ahmed Rezine},
  title     = {Parameterized Tree Systems},
  booktitle = {Formal Techniques for Networked and Distributed Systems
               - FORTE 2008, 28th IFIP WG 6.1 International Conference,
               Tokyo, Japan, June 10-13, 2008, Proceedings},
  year      = {2008},
  pages     = {69-83},
  ee        = {http://dx.doi.org/10.1007/978-3-540-68855-6_5},
  crossref  = {DBLP:conf/forte/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/forte/2008,
  editor    = {Kenji Suzuki and
               Teruo Higashino and
               Keiichi Yasumoto and
               Khaled El-Fakih},
  title     = {Formal Techniques for Networked and Distributed Systems
               - FORTE 2008, 28th IFIP WG 6.1 International Conference,
               Tokyo, Japan, June 10-13, 2008, Proceedings},
  booktitle = {FORTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5048},
  year      = {2008},
  isbn      = {978-3-540-68854-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ictac/AbdullaDR08,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Monotonic Abstraction in Action},
  booktitle = {Theoretical Aspects of Computing - ICTAC 2008, 5th International
               Colloquium, Istanbul, Turkey, September 1-3, 2008. Proceedings},
  year      = {2008},
  pages     = {50-65},
  ee        = {http://dx.doi.org/10.1007/978-3-540-85762-4_4},
  crossref  = {DBLP:conf/ictac/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ictac/2008,
  editor    = {John S. Fitzgerald and
               Anne Elisabeth Haxthausen and
               H{\"u}sn{\"u} Yenig{\"u}n},
  title     = {Theoretical Aspects of Computing - ICTAC 2008, 5th International
               Colloquium, Istanbul, Turkey, September 1-3, 2008. Proceedings},
  booktitle = {ICTAC},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5160},
  year      = {2008},
  isbn      = {978-3-540-85761-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/vmcai/AbdullaHDR08,
  author    = {Parosh Aziz Abdulla and
               Noomene Ben Henda and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Handling Parameterized Systems with Non-atomic Global Conditions},
  booktitle = {Verification, Model Checking, and Abstract Interpretation,
               9th International Conference, VMCAI 2008, San Francisco,
               USA, January 7-9, 2008, Proceedings},
  year      = {2008},
  pages     = {22-36},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78163-9_7},
  crossref  = {DBLP:conf/vmcai/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/vmcai/2008,
  editor    = {Francesco Logozzo and
               Doron Peled and
               Lenore D. Zuck},
  title     = {Verification, Model Checking, and Abstract Interpretation,
               9th International Conference, VMCAI 2008, San Francisco,
               USA, January 7-9, 2008, Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4905},
  year      = {2008},
  isbn      = {978-3-540-78162-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/entcs/AbdullaDR08,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Monotonic Abstraction in Parameterized Verification},
  journal   = {Electronic Notes in Theoretical Computer Science},
  volume    = {223},
  year      = {2008},
  pages     = {3-14},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2008.12.027},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/AbdullaDR07,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Ahmed Rezine},
  title     = {Parameterized Verification of Infinite-State Processes with
               Global Conditions},
  booktitle = {Computer Aided Verification, 19th International Conference,
               CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  year      = {2007},
  pages     = {145-157},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73368-3_17},
  crossref  = {DBLP:conf/cav/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2007,
  editor    = {Werner Damm and
               Holger Hermanns},
  title     = {Computer Aided Verification, 19th International Conference,
               CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4590},
  year      = {2007},
  isbn      = {978-3-540-73367-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@INPROCEEDINGS{Parosh:Bengt:Karlis:Tsay:general,
        Author = "Parosh Aziz Abdulla and Karlis {\v C}er{\=a}ns and Bengt Jonsson
		  and Yih-Kuen Tsay ",
	Title = "General Decidability Theorems for Infinite-State Systems", 
        BookTitle = "Proc.\ LICS '96, 11th IEEE Int.\ Symp.\ on Logic in Computer Science",
        pages= "313-321",
        Year = 1996}


@inproceedings{rmc:transducers,
  author    = {Parosh Aziz Abdulla and
               Giorgio Delzanno and
               Noomene Ben Henda and
               Ahmed Rezine},
  title     = {Regular Model Checking Without Transducers (On Efficient
               Verification of Parameterized Systems)},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems, 13th International Conference, TACAS 2007},
  year      = {2007},
  pages     = {721-736}
}

@Comment , Held               as Part of the Joint European Conferences on Theory and
@Comment                Practice of Software, ETAPS 2007 Braga, Portugal, March
@Comment                24 - April 1, 2007, Proceedings

@Comment   ee        = {http://dx.doi.org/10.1007/978-3-540-71209-1_56},
@Comment   crossref  = {DBLP:conf/tacas/2007},
@Comment   bibsource = {DBLP, http://dblp.uni-trier.de}

@article{cuda:smt,
 author = {Li, Guodong and Gopalakrishnan, Ganesh and Kirby, Robert M. and Quinlan, Dan},
 title = {A symbolic verifier for CUDA programs},
 journal = {SIGPLAN Not.},
 issue_date = {May 2010},
 volume = {45},
 issue = {5},
 month = {January},
 year = {2010},
 issn = {0362-1340},
 pages = {357--358},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/1837853.1693512},
 doi = {http://doi.acm.org/10.1145/1837853.1693512},
 acmid = {1693512},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {cuda, formal verification, spmd, symbolic analysis},
} 

@proceedings{DBLP:conf/tacas/2007,
  editor    = {Orna Grumberg and
               Michael Huth},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 13th International Conference, TACAS 2007, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2007 Braga, Portugal, March
               24 - April 1, 2007, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4424},
  year      = {2007},
  isbn      = {978-3-540-71208-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/concur/AbdullaJRS06,
  author    = {Parosh Aziz Abdulla and
               Bengt Jonsson and
               Ahmed Rezine and
               Mayank Saksena},
  title     = {Proving Liveness by Backwards Reachability},
  booktitle = {CONCUR 2006 - Concurrency Theory, 17th International Conference,
               CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings},
  year      = {2006},
  pages     = {95-109},
  ee        = {http://dx.doi.org/10.1007/11817949_7},
  crossref  = {DBLP:conf/concur/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/concur/2006,
  editor    = {Christel Baier and
               Holger Hermanns},
  title     = {CONCUR 2006 - Concurrency Theory, 17th International Conference,
               CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4137},
  year      = {2006},
  isbn      = {3-540-37376-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/jlp/AbdullaLdR06,
  author    = {Parosh Aziz Abdulla and
               Axel Legay and
               Julien d'Orso and
               Ahmed Rezine},
  title     = {Tree regular model checking: A simulation-based approach},
  journal   = {Journal of Logic and Algebraic Programming},
  volume    = {69},
  number    = {1-2},
  year      = {2006},
  pages     = {93-121},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2006.02.001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tacas/AbdullaLdR05,
  author    = {Parosh Aziz Abdulla and
               Axel Legay and
               Julien d'Orso and
               Ahmed Rezine},
  title     = {Simulation-Based Iteration of Tree Transducers},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems, 11th International Conference, TACAS 2005, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8,
               2005, Proceedings},
  year      = {2005},
  pages     = {30-44},
  ee        = {http://dx.doi.org/10.1007/978-3-540-31980-1_3},
  crossref  = {DBLP:conf/tacas/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2005,
  editor    = {Nicolas Halbwachs and
               Lenore D. Zuck},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 11th International Conference, TACAS 2005, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8,
               2005, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3440},
  year      = {2005},
  isbn      = {3-540-25333-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Finkel:Schnoebelen:everywhere:TCS,
  author = 	 {A. Finkel and {Ph}. Schnoebelen},
  title = 	 {Well-Structured Transition Systems Everywhere!},
  journal = 	 TCS,
  year = 	 2001,
  volume = 	 256,
  number = 	 {1-2},
  pages = 	 {63--92}
}


@conference{dynamic:cuda,
  title={{Automated Dynamic Analysis of CUDA Progr.}},
  author={Boyer, M. and Skadron, K. and Weimer, W.},
  booktitle={3rd Workshop on Software Tools for MultiCore Systems},
  year={2008}
}





@INPROCEEDINGS{gpu:barriers, 
author={Shucai Xiao and Wu-chun Feng}, 
booktitle={Parallel Distributed Processing (IPDPS), 2010 IEEE International Symposium on}, title={Inter-block GPU communication via fast barrier synchronization}, 
year={2010}, 
month={april}, 
volume={}, 
number={}, 
pages={1 -12}, 
keywords={CPU;bitonic sort;dynamic programming;fast Fourier transform;fast barrier synchronization;graphics processing units;inter-block GPU communication;computer graphic equipment;computer graphics;coprocessors;synchronisation;}, 
doi={10.1109/IPDPS.2010.5470477}, 
ISSN={1530-2075},}